desumafandomcom-20200213-history
UMDES Commands
Commands for DESUMA software are listed here. If denoted by X, the command accepts NDFAs with EMPTY_TRACE transitions. If denoted by O, click the command for detailed information and examples. Input/Output Routines create_fsm: Interactive routine to create FSM file. forbid: Writes the list of states that have more than threshold number of individual states. write_ev: Writes all the events in the FSM. write_o: Writes all the observable events in the FSM. write_st: Writes all the states in the FSM. write_uo: Writes all the unobservable events in the FSM. Manipulation of FSM XO acc: Removes inaccessible states from the FSM. change_cprop: Changes controllability properties of events. change_initial_state: Change the initial state of the FSM. change_oprop: Changes observability properties of events. c_par_comp: Creates the constrained parallel composition of the set of FSMs. XO co_acc: Obtains the co-accessible part of the FSM. comp_fsm: Returns the complement of the FSM. concat: Returns the concatenation of the two input FSM's. concat_ev: Adds transitions to the DEAD state for all events in the event list. O conflict: Tests for non-conflicting languages of the two FSM's. equiv: Tests for the language equivalence of two FSM's. incl: Tests if L(H) contains L(G) and if Lm(H) contains Lm(G) where H and G are two input FSM's. inv_p_L: Returns the inverse projection of the FSM with respect to another one and the given event list. X inv_proj: Returns the inverse projection of the FSM with respect to the given event list. live: Returns a live FSM given a non-live one by adding self-loops to all DEAD states. X mark_fsm: Marks all the states in the FSM. minimize_std: Checks for and removes equivalent states from the FSM using the standard algorithm. obsvr: Returns observer of the FSM in diagnoser or FSM format. par_comp: Creates the parallel composition of the set of FMS's. X product: Creates the product of two FSM's. refine: Refines a system model subject to a given speculation model. rename_dead: Renames the DEAD state of an FSM to DEADi. rename_states: Renames the states in the FSM, counting up from 1. rm_state: Removes the listed states from the FSM. union: Creates a machine whose language is the union of two FSM's. Control coobs: Tests for the coobservability of L(H) with respect to L(G), with two agents. coobs_gen: General forms of coobs dealing with multiple site and generalized coobservability. ctrb: Tests for the controllability of L_m(H) with respect to L(G) and a set of uncontrollable events. enable_map: Lists events that are enabled or disables at each state of a supervisor FSM with respect to a system FSM. infcon: Generates the infimal prefix-closed and controllable super-language of a given language with respect to a second prefix-closed language. normal: Tests for the normality of L(H) with respect to L(G). obs: Tests for the observability of L(H) with respect to L(G). supcn: Builds the supremal controllable normal sublanguage of L_m(H) with respect to L(G). supcn_pc: Builds the supremal controllable normal sublanguage of L(H) with respect to L(G). supcon1: Builds the supremal controllable sublanguage of L_m(H) with respect to L(G). supcon_std. Builds the supremal controllable sublanguage of L(H) with respect to L(G). supnorm: Builds the supremal controllable sublanguage of L_m(H) with respect to L(G). ylp_s: Builds an FSM, H_sup.fsm, whose marked language is the supremal controllable sublanguage of the intersection of Lm(G) and Lm(H) with respect to L(G) and E{uc}, the uncontrollable event set of G. Failure Diagnosis compose: Generates the composite system with the appropriate sensor readings for each state. diag: Generates the (multiple fault) diagnoser for the given FSM. diag_a: Generates the diagnoser (with ambiguous labels) for the FSM. diag_EX: Generates the extended diagnoser for the FSM. diag_UR: Generates the diagnoser with unobservable reach. r_cycle: Tests for diagnosability of an intermittent-fault FSM by looking for type o, type i, type p and type r indeterminate cycles. idiag: Generates the I-diagnoser of the FSM. dicycle: Tests for I-diagnosability of the FSM by detecting (Fi,li)-indeterminate cycles. dcycle: Tests for diagnosability of the FSM by detecting Fi-indeterminate cycles. eventmap: Maps the indicator events to the observable states in the FSM. r_diag: Builds a diagnoser that can handle reset events. sensmap: Maps the sensor readings to every state in the FSM. verifier_dia: Builds verifiers to test diagnosibility. verifier_decen_dia: Builds verifiers to test diagnosibility in a decentralized system. Stochastic Diagnosability a_diagnosability: Tests for A-Diagnosability by looking at the given FSM's stochastic diagnoser. create_sfsm: Interactive routine to create stochastic information files for an existing FSM. sdiag: Generates the stochastic diagnoser for the given FSM.